[]!P(sys) == (run:Run. sys(run)) & (run:Run. sys(run)  P(run)) 

latex

---

clarification:

box!(Run;P)(sys) == (run:Run. sys(run)) & (run:Run. sys(run)  P(run)) 

latex

Definitions	P & Q, x:A. B(x), x:A. B(x), P  Q
FDL editor aliases	box!